(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_NRA)
(declare-fun v0 () Real)
(declare-fun v1 () Real)
(declare-fun v2 () Real)
(assert (let ((e3 1))
(let ((e4 1))
(let ((e5 0))
(let ((e6 (- v0 v2)))
(let ((e7 (- e6 v2)))
(let ((e8 (- v0)))
(let ((e9 (- e7 e8)))
(let ((e10 (/ e3 e3)))
(let ((e11 (- e6 e8)))
(let ((e12 (* e7 e5)))
(let ((e13 (- v0 v0)))
(let ((e14 (+ e7 e13)))
(let ((e15 (* (- e5) e10)))
(let ((e16 (* e6 e14)))
(let ((e17 (* (- e4) e13)))
(let ((e18 (/ e4 (- e4))))
(let ((e19 (/ e4 e4)))
(let ((e20 (- e9)))
(let ((e21 (+ e10 e18)))
(let ((e22 (/ e4 (- e4))))
(let ((e23 (- e13)))
(let ((e24 (- e18 e18)))
(let ((e25 (- e10 e22)))
(let ((e26 (/ e5 e3)))
(let ((e27 (- e6 v0)))
(let ((e28 (- e22 e22)))
(let ((e29 (- e11)))
(let ((e30 (- e18 e20)))
(let ((e31 (+ e8 e17)))
(let ((e32 (- v0)))
(let ((e33 (- e31 e21)))
(let ((e34 (* e25 v0)))
(let ((e35 (/ e5 (- e3))))
(let ((e36 (+ v1 e6)))
(let ((e37 (distinct e22 e13)))
(let ((e38 (>= v2 e36)))
(let ((e39 (< e8 e21)))
(let ((e40 (> e10 e36)))
(let ((e41 (= e35 e10)))
(let ((e42 (< e9 e30)))
(let ((e43 (= e16 v1)))
(let ((e44 (> e20 e35)))
(let ((e45 (distinct e11 e16)))
(let ((e46 (< e24 e28)))
(let ((e47 (<= v1 e14)))
(let ((e48 (>= e28 e6)))
(let ((e49 (distinct e8 e12)))
(let ((e50 (>= e18 e24)))
(let ((e51 (> e31 e23)))
(let ((e52 (< e8 v0)))
(let ((e53 (>= e8 v1)))
(let ((e54 (> v0 e8)))
(let ((e55 (distinct v0 e35)))
(let ((e56 (> e7 e19)))
(let ((e57 (>= e15 e8)))
(let ((e58 (>= e34 e14)))
(let ((e59 (<= e24 e16)))
(let ((e60 (<= e16 e17)))
(let ((e61 (>= e20 e10)))
(let ((e62 (>= e16 e36)))
(let ((e63 (= e13 e34)))
(let ((e64 (> e17 v1)))
(let ((e65 (> e7 e32)))
(let ((e66 (<= e11 e13)))
(let ((e67 (<= e16 e7)))
(let ((e68 (<= e19 e34)))
(let ((e69 (>= v1 e14)))
(let ((e70 (<= e33 e15)))
(let ((e71 (>= e7 e16)))
(let ((e72 (<= e17 e24)))
(let ((e73 (> e17 e24)))
(let ((e74 (>= e28 e9)))
(let ((e75 (>= e15 e9)))
(let ((e76 (>= e30 e9)))
(let ((e77 (>= e10 e6)))
(let ((e78 (<= e15 e10)))
(let ((e79 (<= e28 e16)))
(let ((e80 (> e24 e32)))
(let ((e81 (>= e34 e8)))
(let ((e82 (>= e27 e7)))
(let ((e83 (< e15 e12)))
(let ((e84 (<= e10 e26)))
(let ((e85 (< e11 e10)))
(let ((e86 (> e9 v0)))
(let ((e87 (<= e7 e23)))
(let ((e88 (> e26 e7)))
(let ((e89 (>= e11 v2)))
(let ((e90 (< e18 e11)))
(let ((e91 (distinct e27 e26)))
(let ((e92 (= e19 e6)))
(let ((e93 (distinct e17 v0)))
(let ((e94 (= e29 v1)))
(let ((e95 (> e36 v0)))
(let ((e96 (< e8 e6)))
(let ((e97 (= e35 e19)))
(let ((e98 (>= e35 e11)))
(let ((e99 (> e17 e27)))
(let ((e100 (distinct e21 e24)))
(let ((e101 (< e28 e12)))
(let ((e102 (= e24 e6)))
(let ((e103 (<= e32 e30)))
(let ((e104 (<= e27 v1)))
(let ((e105 (> e6 e29)))
(let ((e106 (= e6 e13)))
(let ((e107 (<= e14 e16)))
(let ((e108 (= e20 v0)))
(let ((e109 (<= e36 e15)))
(let ((e110 (= e27 e17)))
(let ((e111 (= e24 e13)))
(let ((e112 (< e17 e33)))
(let ((e113 (>= e28 e34)))
(let ((e114 (< e16 v0)))
(let ((e115 (< e8 e23)))
(let ((e116 (= e18 e22)))
(let ((e117 (<= e22 e32)))
(let ((e118 (distinct e32 e17)))
(let ((e119 (> e32 v1)))
(let ((e120 (> v0 e29)))
(let ((e121 (= e36 e17)))
(let ((e122 (distinct e11 e31)))
(let ((e123 (>= v0 e21)))
(let ((e124 (< e33 e13)))
(let ((e125 (< e21 v2)))
(let ((e126 (< e6 e34)))
(let ((e127 (>= e14 e21)))
(let ((e128 (< e6 e36)))
(let ((e129 (< e11 e32)))
(let ((e130 (= v2 e34)))
(let ((e131 (<= e21 e26)))
(let ((e132 (= e14 e8)))
(let ((e133 (< e26 v1)))
(let ((e134 (> e12 e21)))
(let ((e135 (<= e35 e21)))
(let ((e136 (< e15 e18)))
(let ((e137 (> e36 e13)))
(let ((e138 (= e8 e36)))
(let ((e139 (= e19 e33)))
(let ((e140 (< e22 v1)))
(let ((e141 (distinct e36 e19)))
(let ((e142 (< e22 e30)))
(let ((e143 (distinct e25 e7)))
(let ((e144 (<= e9 e28)))
(let ((e145 (<= e9 e9)))
(let ((e146 (distinct e9 e13)))
(let ((e147 (< e26 e12)))
(let ((e148 (>= e33 e12)))
(let ((e149 (<= e16 e30)))
(let ((e150 (< e12 e24)))
(let ((e151 (= e9 e17)))
(let ((e152 (> e27 e25)))
(let ((e153 (< e35 e13)))
(let ((e154 (<= e11 e34)))
(let ((e155 (< e33 e19)))
(let ((e156 (= e16 e23)))
(let ((e157 (> e15 v2)))
(let ((e158 (< e24 e8)))
(let ((e159 (>= e17 e21)))
(let ((e160 (>= e16 e22)))
(let ((e161 (> e10 v1)))
(let ((e162 (= e20 e31)))
(let ((e163 (<= e33 e34)))
(let ((e164 (< e17 e21)))
(let ((e165 (distinct e25 e20)))
(let ((e166 (> e28 v1)))
(let ((e167 (> e11 v2)))
(let ((e168 (<= e33 e15)))
(let ((e169 (>= e18 e28)))
(let ((e170 (< e24 e32)))
(let ((e171 (> e7 v1)))
(let ((e172 (distinct e10 e16)))
(let ((e173 (distinct e29 e21)))
(let ((e174 (<= e23 e21)))
(let ((e175 (>= e24 e35)))
(let ((e176 (distinct v0 e16)))
(let ((e177 (= e33 e29)))
(let ((e178 (<= e13 e36)))
(let ((e179 (<= e26 e13)))
(let ((e180 (= e32 e32)))
(let ((e181 (distinct e7 e19)))
(let ((e182 (distinct e12 e35)))
(let ((e183 (= e15 e14)))
(let ((e184 (< e30 e11)))
(let ((e185 (>= e24 e14)))
(let ((e186 (>= e20 e9)))
(let ((e187 (<= e22 e33)))
(let ((e188 (= e10 e30)))
(let ((e189 (< e23 e9)))
(let ((e190 (= e17 e25)))
(let ((e191 (>= e6 e24)))
(let ((e192 (= e138 e63)))
(let ((e193 (ite e148 e158 e95)))
(let ((e194 (=> e180 e96)))
(let ((e195 (ite e182 e89 e159)))
(let ((e196 (and e54 e105)))
(let ((e197 (or e178 e167)))
(let ((e198 (and e128 e196)))
(let ((e199 (not e157)))
(let ((e200 (or e136 e150)))
(let ((e201 (and e61 e118)))
(let ((e202 (xor e49 e124)))
(let ((e203 (or e40 e43)))
(let ((e204 (=> e94 e203)))
(let ((e205 (and e114 e143)))
(let ((e206 (= e168 e50)))
(let ((e207 (or e174 e77)))
(let ((e208 (=> e154 e202)))
(let ((e209 (or e100 e117)))
(let ((e210 (=> e85 e67)))
(let ((e211 (or e169 e47)))
(let ((e212 (or e110 e163)))
(let ((e213 (or e127 e204)))
(let ((e214 (= e206 e62)))
(let ((e215 (or e81 e164)))
(let ((e216 (=> e122 e183)))
(let ((e217 (or e64 e151)))
(let ((e218 (=> e161 e87)))
(let ((e219 (= e130 e101)))
(let ((e220 (not e213)))
(let ((e221 (not e129)))
(let ((e222 (or e104 e104)))
(let ((e223 (= e175 e195)))
(let ((e224 (ite e215 e155 e88)))
(let ((e225 (ite e208 e45 e209)))
(let ((e226 (= e179 e82)))
(let ((e227 (=> e70 e144)))
(let ((e228 (= e147 e132)))
(let ((e229 (xor e198 e188)))
(let ((e230 (or e97 e71)))
(let ((e231 (= e218 e171)))
(let ((e232 (or e226 e134)))
(let ((e233 (xor e60 e227)))
(let ((e234 (= e186 e58)))
(let ((e235 (or e115 e228)))
(let ((e236 (=> e57 e152)))
(let ((e237 (and e78 e140)))
(let ((e238 (or e53 e73)))
(let ((e239 (and e214 e190)))
(let ((e240 (and e230 e46)))
(let ((e241 (not e56)))
(let ((e242 (or e166 e173)))
(let ((e243 (and e229 e91)))
(let ((e244 (xor e51 e86)))
(let ((e245 (=> e137 e221)))
(let ((e246 (xor e65 e219)))
(let ((e247 (=> e39 e233)))
(let ((e248 (and e146 e191)))
(let ((e249 (= e41 e192)))
(let ((e250 (not e76)))
(let ((e251 (=> e243 e212)))
(let ((e252 (or e107 e42)))
(let ((e253 (and e38 e220)))
(let ((e254 (or e92 e84)))
(let ((e255 (= e199 e120)))
(let ((e256 (ite e52 e72 e236)))
(let ((e257 (xor e187 e59)))
(let ((e258 (xor e200 e145)))
(let ((e259 (ite e252 e142 e156)))
(let ((e260 (=> e246 e141)))
(let ((e261 (= e245 e165)))
(let ((e262 (ite e189 e238 e90)))
(let ((e263 (= e248 e210)))
(let ((e264 (ite e197 e83 e121)))
(let ((e265 (= e194 e162)))
(let ((e266 (or e211 e222)))
(let ((e267 (ite e235 e249 e262)))
(let ((e268 (=> e112 e109)))
(let ((e269 (and e225 e37)))
(let ((e270 (=> e256 e247)))
(let ((e271 (or e263 e253)))
(let ((e272 (not e271)))
(let ((e273 (=> e153 e149)))
(let ((e274 (ite e231 e244 e131)))
(let ((e275 (ite e66 e55 e201)))
(let ((e276 (not e264)))
(let ((e277 (= e75 e275)))
(let ((e278 (and e181 e184)))
(let ((e279 (or e79 e217)))
(let ((e280 (not e237)))
(let ((e281 (and e257 e251)))
(let ((e282 (ite e111 e261 e170)))
(let ((e283 (xor e123 e119)))
(let ((e284 (and e268 e270)))
(let ((e285 (= e283 e207)))
(let ((e286 (xor e259 e276)))
(let ((e287 (= e116 e240)))
(let ((e288 (and e133 e99)))
(let ((e289 (=> e242 e177)))
(let ((e290 (xor e44 e139)))
(let ((e291 (or e260 e281)))
(let ((e292 (=> e255 e126)))
(let ((e293 (not e48)))
(let ((e294 (ite e241 e205 e239)))
(let ((e295 (not e282)))
(let ((e296 (=> e269 e69)))
(let ((e297 (xor e172 e294)))
(let ((e298 (= e292 e277)))
(let ((e299 (and e113 e160)))
(let ((e300 (xor e295 e68)))
(let ((e301 (=> e293 e258)))
(let ((e302 (and e193 e103)))
(let ((e303 (or e284 e98)))
(let ((e304 (=> e232 e289)))
(let ((e305 (ite e250 e302 e250)))
(let ((e306 (and e290 e301)))
(let ((e307 (xor e93 e299)))
(let ((e308 (and e74 e303)))
(let ((e309 (=> e223 e254)))
(let ((e310 (or e304 e309)))
(let ((e311 (ite e300 e135 e234)))
(let ((e312 (xor e102 e102)))
(let ((e313 (= e224 e265)))
(let ((e314 (or e108 e285)))
(let ((e315 (or e216 e313)))
(let ((e316 (and e315 e310)))
(let ((e317 (or e266 e267)))
(let ((e318 (and e297 e297)))
(let ((e319 (and e298 e272)))
(let ((e320 (not e319)))
(let ((e321 (or e125 e278)))
(let ((e322 (ite e296 e305 e296)))
(let ((e323 (or e317 e306)))
(let ((e324 (or e106 e307)))
(let ((e325 (ite e311 e320 e280)))
(let ((e326 (or e323 e176)))
(let ((e327 (=> e286 e273)))
(let ((e328 (not e274)))
(let ((e329 (and e312 e279)))
(let ((e330 (or e318 e314)))
(let ((e331 (ite e291 e329 e185)))
(let ((e332 (xor e325 e308)))
(let ((e333 (or e332 e316)))
(let ((e334 (= e328 e287)))
(let ((e335 (= e327 e334)))
(let ((e336 (xor e333 e326)))
(let ((e337 (xor e335 e80)))
(let ((e338 (=> e322 e331)))
(let ((e339 (ite e288 e338 e330)))
(let ((e340 (xor e321 e324)))
(let ((e341 (not e336)))
(let ((e342 (or e337 e339)))
(let ((e343 (not e342)))
(let ((e344 (not e341)))
(let ((e345 (ite e344 e343 e343)))
(let ((e346 (and e345 e340)))
e346
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
